the_w:World. Msg  Type 

latex

Definitions	World, Msg, w.M, Msg(M), x:A. B(x), t  T
Lemmas	Msg wf, world wf